\documentclass{article}
\usepackage{xcolor} 
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{proof}
\usepackage{amsthm}
%\usepackage{fullpage}
\usepackage{hyperref}
\usepackage{caption}
\usepackage{comment}
\usepackage{subcaption}
\usepackage{fancybox}
%\usepackage{diagrams}
\usepackage{stmaryrd}
\definecolor{light-gray}{gray}{0.86}
\newcommand{\nil}[0]{\mathsf{nil}} 
\newcommand{\cons}[0]{\mathsf{cons}} 
\newcommand{\vecc}[0]{\mathsf{vec}} 
\newcommand{\suc}[0]{\mathsf{S}} 
\newcommand{\nat}[0]{\mathsf{Nat}} 
\newcommand{\ind}[0]{\mathsf{Ind}} 
\newcommand{\app}[0]{\mathsf{app}} 

\newcommand{\selfstar}[0]{$\mathsf{Selfstar}\ $} 
\newcommand{\self}[0]{\mathbf{S}} 
\newcommand{\fomega}[0]{\mathbf{F}_{\omega}} 
\newcommand{\cc}[0]{\mathbf{CC}} 
\newcommand{\gray}[1]{\colorbox{light-gray}{#1}}
\newcommand{\mgray}[1]{\colorbox{light-gray}{$#1$}}
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\Mb}[4]{
\{#1_i:#4_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\interp}[1]{\llbracket #1 \rrbracket} 
\newcommand{\mylet}[2]{\mathbf{let}\ #1 \ \mathbf{in} \ #2} 
\newcommand{\mycase}[2]{\mathbf{case}\ #1 \ \mathbf{of} \ \{ #2 \}_{i\in {N}}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 ---Frank]}}}

\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
% for page numbers:
\pagestyle{plain}

\begin{document}
\title{Totality Proof Synthesis for Primitive Recursion}

\author{Peng Fu}



\maketitle

\begin{abstract}
  The goal of this work is automatically generate totality proof of annoying functions likes
  Ackermann function and its company. 
\end{abstract}
\section{Specification} 
Let us remind ourself the definition of primitive recursion and the notion of lambda definability. Note that we will use Church encoded data through out this article.  
\begin{definition}[Algebraic Data Type]

\end{definition}

\begin{definition}[Initial Functions]
\

\begin{itemize}
  \item Selection function $U^n_i(x_1, ..., x_n) = x_i$.
   \item Constant function $C(x) = c$ where $c$ is a nullary data constructor. 
   \item All Non-nullary Data type constructors. 
  \end{itemize}
\end{definition}  

\begin{definition}[Primitive Recursion]
\

  \begin{itemize}
  \item Initial function is primitive recursive.
  \item If $f(\vec{n}) = \chi(\psi_1(\vec{n}), ..., \psi_n(\vec{n}))$ and $\chi, \psi_1,..., \psi_n$ are primitive recursive, then $f$ is primitive recursive. 
  \item Let $f(a_i(x_{i1},..., x_{ik},b_{i1},...,b_{im}), \vec{n} ) = \phi(x_{i1},..., x_{ik}, b_{i1},...,b_{im},\vec{n}, f(b_{i1}, \vec{n}), ...,  f(b_{im}, \vec{n}))$ for all data constructor $\{a_i : A_{i1} \to ... \to A_{ik} \to \underbrace{D \to ... \to D}_{m} \to D\}_{i\in N}$ of datatype $D$ given $ x_{i1} : A_{i1}, ..., x_{ik}: A_{ik}$ and $b_{i1},...,b_{im} : D$, where $k, m \geq 0$. If $\phi, g$ are primitive recursive, then $f$ is primitive recursive. 
  \end{itemize}

\end{definition}

\begin{definition}[Lambda Definability]
  A function $f : D_1 \to D_2$ is lambda definable if for any lambda term $t$ represents 
  an element $ a \in D_1$, there is a lambda term $\phi_f$ such that $\phi_f\ t$ is a lambda
  term represent $f(a) \in D_2$. 
\end{definition}
Note that the definition of lambda definability can be extended to multi-arity function thanks
to Currying in lambda calculus. 

\section{Kleene Conversion}

\begin{lemma}
  \label{const}
  Data type constructors are lambda definable through Church encoding. 
\end{lemma}
Note that we will use the same letter/symbol to represent data type constructor and its lambda
representation. 
\begin{lemma}
  Primitive recursive function are lambda definable.
\end{lemma}
\begin{proof}
  \
  
  \textit{Initial functions}. $U_i^n$ is definable by lambda term $\lambda x_1... x_n. x_i$. Constant function is definable by $\lambda x. \bar{c}$. And by lemma \ref{const} we know that data type constructors
  are lambda definable.
  
  \
  
  \textit{Composition}. For $f(\vec{n}) = \chi(\psi_1(\vec{n}), ..., \psi_n(\vec{n}))$ and $\chi, \psi_1,..., \psi_n$ are lambda definable by $\bar{\chi}, \bar{\psi_1},..., \bar{\psi_n}$, then $f$ is lambda definable by $\lambda \vec{x}.\bar{\chi} (\bar{\psi_1} \vec{x})...(\bar{\psi_n}\vec{x})$.
  
  \
  
  \textit{Primitive Recursion}. Let $f(a_i(x_{i1},..., x_{ik},b_{i1},...,b_{im}), \vec{n} ) = \phi(x_{i1},..., x_{ik}, b_{i1},...,b_{im},\vec{n}, f(b_{i1}, \vec{n}), ...,  f(b_{im}, \vec{n}))$ for all data constructor $\{a_i : A_{i1} \to ... \to A_{ik} \to \underbrace{D \to ... \to D}_{m} \to D\}_{i\in N}$ of datatype $D$ given $ x_{i1} : A_{i1}, ..., x_{ik}: A_{ik}$ and $b_{i1},...,b_{im} : D$, where $k, m \geq 0$. Suppose $\phi, g$ are lambda definable by $\bar{\phi}$. Let $H_i := \lambda \vec{n} x_1, ..., x_k p_1 ... p_m . \langle a_i x_1... x_k (\pi_1 p_1) ... (\pi_1 p_m), \bar{\phi} x_1...  x_k (\pi_1 p_1) ... (\pi_1 p_m) \vec{n} (\pi_2 p_1) ... (\pi_2 p_m) \rangle$.  Then $f := \lambda  x \vec{n} . x (H_1 \vec{n}) ... (H_n \vec{n})$. For simplicity, let us consider only unary function $f$. So $f = \lambda  x . x H_1 ... H_n$. We need to prove for any $t$ represent $a \in D$, 
\end{proof}

\section{Proof Annotation}



\cite{Abadi:93}.
\bibliographystyle{plain}

% The bibliography should be embedded for final submission.
\bibliography{paper}

\end{document}
